COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	block.ax[f83,jmc]	Axioms for building structures from blocks
C00013 ENDMK
C⊗;
block.ax[f83,jmc]	Axioms for building structures from blocks

is_stub(tower,structure,s): tower exists in  s  and is a stub
of one of the towers of structure.

is_stub(to,st,s) ≡ member(to,structure s) 
	∧ ∃to1.(is_stub1(to,to1) ∧ member(to1,st))

This has the objection that it presumes the function  structure s.  This
would be ok if we regard  s  as the state of the table, but if we want
to consider  s  as a general situation, there isn't any such thing as
the structure of  s.  So we can rewrite it as

is_stub(to,st,s) ≡ ∃st1.present(st1,s) ∧ member(to,st1) 
	∧ ∃to1.(is_stub1(to,to1) ∧ member(to1,st))

present(st,s):		The structure  st  is present in the situation  s.
It isn't clear whether this should assert that  st  is the complete
structure present in  s.  Presumably this would be necessary if we
ever wanted to prove that some other structure could not be built.

member(to,st):		The tower  to  is part of the structure  st.

is_stub1(to,to1):	The tower  to  is a stub of the tower  to1.

∀to.is_stub1(to,to)

∀to to1 b.is_stub1(to,to1) ⊃ is_stub1(to,b.to1)

clear(b,s):		The block  b  is clear in the situation  s.

placeable(b,st,s):	The block  b  can be placed in its desired final
position in making the structure  st  in the situation  s.

placeable(b,st,s) ≡ clear(b,s) ∧ is_stub(stub(b,st),st,s)

∀b st.is_stub1(b.stub(b,st),st)

Perhaps it's better to make the stub on which  b  is to be placed an
argument of  placeable.  We would then have

placeable(b,l,st,s) ≡ clear(b,s) ∧ is_stub1(l,to) ∧ member(to,st)
∧ present(st,s) ∧ clear(l,s)

***** start over

clear(b,s):		The block  b  is clear.  By this we mean clear
in the situation  s,  but we will suppress mentioning situation arguments
in the English description of the functions and predicates.

present(to,s):		The tower  to  is present.  It
is sitting on the table, but it may have more blocks on top of it.

present1(to,st):	The tower to belongs to the structure  st.
It is sitting on the table in  st,  but it may have more blocks on
top of it.

top to:			The top block of tower  to.  In our presently
intended representation  top to = car to.

movable(b,to,s):	The block  b  is movable onto the tower  to.

movable(b,to,s) ≡ clear(b,s) ∧ present(to,s) ∧ clear(top to,s)

Using the predicates  present  and  present1 emphasizes the parallel
between structures and situations.  The difference is that we think
of a situation as open ended; they are infinitely rich in aspects
we don't know about.  However, if we limit our consideration of a
situation to the structure that happens to be on the table in it,
then there is a parallel between a desired structure  st  and the
situation.  We can and perhaps should emphasize this parallel
further by considering actions on structures and supposing that
certain actions in a situation correspond to actions in the structure.
However, this seems to be a separate issue from the one concerning
us now.

For now we should identify structures and situations, since the
problems of forward reasoning are the same.

goodmove(action,goal,s):	action  is a possible and appropriate
move for achieving  goal.

movable(b,to,s):	b can be immediately moved to  to.

musttable(b,st,s,b1):	In order to build  st, it is necesary to move
b  to the table.  b1  is a "witness" of this, i.e. a block that will
be below  b  in the final tower.

movable(b,to,s) ∧ stub1(b.to,st) ⊃ goodmove(move(b,t0),make(st),s)

musttable(b,st,s,b1) ≡ above(b,b1,st) ∧ above(b,b1,s)
∧ stub(b,st) ≠ stub(b,s)

musttable(b,st,s,b1) ∧ clear(b,s) ⊃ goodmove(move(b,Table),make(st),s)

Suppose we write  must(move(b,Table),make(st),s) instead of
musttable(b,st,s,b1),  which
uses a general predicate  must(action,goal,situation).  What we mean
is that the action must be performed eventually in some successor
of the situation  s.  It may not even be legal in  s,  but note that
it involves identification of moves across situations.

The axioms are then

must(move(b,Table),make(st),s) ≡ 
	∃b1.above(b,b1,st) ∧ above(b,b1,s) ∧ stub(b,st) ≠ stub(b,s)

and

	must(a,g,s) ∧ possible(a,s) ⊃ goodmove(a,g,s)

with

possible(move(b,Table),s) ≡ clear(b,s).

Actually these are axioms for the operating reasoner.  The ab initio reasoner
which we can regard as playing a role similar to that of a compiler should
deduce these as theorems from the basic blocks axioms.

Now for planning.

	The towers of a desired structure can be built one at at time,
and it is never necessary to dismantle a tower that has been built.
Because it is not a fact about the world in general that goals, once
achieved, never have to be undone, the fact in this case should be
represented as an axiom or theorem rather than being built into the
formalism.

Questions:

1. Shall we represent a structure as a set of towers or as a list of
towers.  From the point of view of semantics a set is better.  There is
no particular reason to consider the towers as being in a definite order.

splits(st,to,st1):	The structure  st  splits into the tower  to
and the remaining structure  st1.

splits(st,to,st1) ∧ plan_for(make(st1),pl1) ∧ plan_for(make(to),pl)
	⊃ plan_for(make(st),pl & pl1)

achieves(plan,goal,s) ∧ advances(action,plan,s) ⊃ goodmove(action,goal,s)

splits(st,to,st1) ∧ achieves(pl,make(to),s)
		 ⊃ achieves(pl+goal(make(st1)),make(st),s)


Another approach

goal(make(st),s) ∧ ¬done(make(st),s) ∧ splits(st,to,st1) ∧ ¬present(to,s)
	 ⊃ goal(make(to),s)

done(g,s):		The goal g  has been achieved in situation  s.
			¬done(g,s) is established non-monotonically.

goal(make(to),s) ∧ ¬done(make(to),s) ∧ is_done_part(to1,to,s) ∧ covers(b,to1,to)
		⊃ goal(move(b,to1),s)

is_done_part(to1,to,s):		Tower  to1  is the part of tower  to  that has
been completed in situation  s.

covers(b,to1,to):	Block  b  is just above tower  to1  in tower  to.

Although there are doubts about  goal(g,s),  we will proceed that way
for the time being.  The doubt is that perhaps the right predicate is
something like  furthers(g1,g2,s).

goal(g,s)		: g  is a goal.

furthers(g1,g2,s)	: achieving  g1  furthers achieving  g2.

¬done(make(to),s) ∧ is_done_part(to,s) = to1 ∧ covers(b,to1,s)
		⊃ furthers(move(b,to1),s)

¬done(clear(b),s) ⊃ furthers(clear(b),move(b,to1),s)

¬done(clear(top(to1)),s) ⊃ furthers(clear(top(to1)),move(b,to1),s)

above(b1,b,s) ⊃ furthers(move(b1,Table),move(b,l),s)